\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:ecl(${\it ds}$; ${\it da}$), $L$:(event{-}info(${\it ds}$;${\it da}$) List).
\\[0ex](ecl{-}trans{-}normal(ecl{-}trans($x$))
\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}^{+}$. \+
\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; ecl{-}trans($x$))($n$,$L$)) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es(ecl{-}trans($x$)))))
\-\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\wedge$ (ecl{-}halt(${\it ds}$; ${\it da}$; $x$)($n$,${\it L'}$))))
\-\\[0ex]$\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; ecl{-}trans($x$))($n$,$L$)))
\-\\[0ex]$\wedge$ ($\forall$$m$:$\mathbb{N}$. (ecl{-}act(${\it ds}$; ${\it da}$; $m$; $x$)($L$)) $\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}act(${\it ds}$; ${\it da}$; ecl{-}trans($x$))($m$,$L$)))
\end{tabbing}